bframe-p(es; i; k; L)
== alle-at(es; i; e.((es-kind(es; e) = k)  (l:IdLnk. ((l  L))  (es-sends(es; l; e) = [])))
== alle-at() 

latex

---

clarification:

bframe-p(es; i; k; L)
== alle-at(es;
== alle-at(i;
== alle-at(e.((es-kind(es; e) = k  Knd)
== alle-at( (l:IdLnk. ((l  L  IdLnk))  (es-sends(es; l; e) = []  (es-Msg(es) List))))
== alle-at() 

latex

Definitions	alle-at(es; i; e.P(e)), Knd, es-kind(es; e), x:A. B(x), P  Q, A, (x  l), IdLnk, s = t, type List, es-Msg(es), es-sends(es; l; e), []
FDL editor aliases	bframe-p